$\forall$$M$:(IdLnk$\rightarrow$Id$\rightarrow$Type), $m$:Msg($M$). mlnk($m$) $\in$ IdLnk